A:Type, eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L) 

latex

Definitions	p  q, eqof(d), deq-member(eq;x;L), Prop, P  Q, {T}, False, P  Q, P & Q, b, P  Q, P  Q, (x  l), EqDecider(T), x:A. B(x), t  T
Lemmas	deq wf, nil member, l member wf, assert wf, deq-member wf, eqof wf, bor wf, deq property, or functionality wrt iff, iff functionality wrt iff, cons member, assert of bor